/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.symm;

import java.util.Map;
import java.util.Set;

import alloy.bool.BooleanFormula;
import alloy.subscope.ScopedSigsInfo;
import alloy.transl.ASTInfo;
import alloy.transl.RelationAllocator;
import alloy.transl.TranslInfo;
import alloy.util.Params;

/**
 * Coordinates symmetry breaking: invokes implementations various {@link SymmetryBreakingMethod}s in
 * a sequence to generate a symmetry-breaking predicate.
 * <p>
 * Symmetry-breaking uses interchangeability of atoms within each basic type
 * to speed up the search for models.   Create a
 * <em>symmetry-breaking predicate</em>: a {@link BooleanFormula}
 * that is <code>true</code> of at least one model instance
 * per symmetry class.  A separate instance of {@link SymmetryBreaker}
 * is created by each call to {@link alloy.api.AlloyRunner#_analyzeCommand}.
 *
 * @see http://sdg.lcs.mit.edu/~ilya_shl/symmetry
 */
public class SymmetryBreaker {
    /** Information about the translatable AST */
    private final ASTInfo _astInfo;

    /** The set of all basic types */
    private final Set /* of BasicType */ _allBasicTypes;

    /** The relation allocator we use to allocate Boolean variables to relations */
    private final RelationAllocator _relAlloc;

    /** Information on how much symmetry is left in each basic type */
    private final AvailableSymmetry _availSymm;

    /** The symmetry-breaking predicate we are constructing */
    private final SymmetryBreakingPredicate _sbp = new SymmetryBreakingPredicate();

    //////////////
    // Methods //
    ////////////
    

    /** Construct the SymmetryBreaker object, don't break any symmetries yet */
    public SymmetryBreaker(ASTInfo astInfo_, RelationAllocator relAlloc_) {
	_astInfo = astInfo_;
	_relAlloc = relAlloc_;
	_allBasicTypes = astInfo_.getBasicTypes();
	_availSymm = new AvailableSymmetry(_allBasicTypes);
    }


    /**
     * Break symmetries before translation.  At this point we have allocated Boolean variables
     * to relation tuples, so we have the translation of each relation, but we have not translated
     * any non-leaf AST nodes.  
     */
    public void breakSymmsBeforeTranslation(ScopedSigsInfo sigsInfo_,
					    Map /* LeafId->Integer */ leafId2scope_,
					    Map /* LeafId->ExprRelationInfo */ id2Annotation_) {
	// Break total-order symmetry
	SBM_Ord sbmOrd = new SBM_Ord(_astInfo, _relAlloc);
	_sbp.conjoin(sbmOrd.breakSymmetry(_availSymm, _allBasicTypes));
	_relAlloc.simplify(_sbp.getUnitClauses());

	// Break subscope symmetry
	if (Params.glob.getBoolParam("SYMM", "subscopes", false)) {
	    SBM_Subscopes sbmSubscopes = new SBM_Subscopes(_astInfo,
							   _relAlloc,
							   sigsInfo_,
							   leafId2scope_,
							   id2Annotation_);
	    
	    _sbp.conjoin(sbmSubscopes.breakSymmetry(_availSymm, _allBasicTypes));
	    _relAlloc.simplify(_sbp.getUnitClauses());
	}

	// Break disjoint-singletons symmetry
	if (Params.glob.getBoolParam("SYMM", "disjSing", false)) {
	    SBM_DisjSingletons disjSingletons = new SBM_DisjSingletons(_astInfo, _relAlloc);
	    _sbp.conjoin(disjSingletons.breakSymmetry(_availSymm, _allBasicTypes));
	    _relAlloc.simplify(_sbp.getUnitClauses());
	}
		
	// Break DAG symmetry
	SBM_DAG sbmDAG = new SBM_DAG(_astInfo, _relAlloc, true /* only leaf DAGs */);
	_sbp.conjoin(sbmDAG.breakSymmetry(_availSymm, _allBasicTypes));
	_relAlloc.simplify(_sbp.getUnitClauses());

	// Break lexicographical-order symmetry
	SBM_LexLeader sbmLexLeader = new SBM_LexLeader(_astInfo, _relAlloc);
	_sbp.conjoin(sbmLexLeader.breakSymmetry(_availSymm, _allBasicTypes));
	_relAlloc.simplify(_sbp.getUnitClauses());

    }  // breakSymmsBeforeTranslation()


    public void  breakSymmsAfterTranslation(TranslInfo translInfo_) {
	// Break DAG symmetry
	SBM_DAG sbmDAG = new SBM_DAG(translInfo_, _relAlloc, false /* use Expr DAGs */);
	_sbp.conjoin(sbmDAG.breakSymmetry(_availSymm, _allBasicTypes));
	_relAlloc.simplify(_sbp.getUnitClauses());
    }

    public BooleanFormula getSymmetryBreakingPredicate() {
	return _sbp.getSymmBrkPredicate();
    }
}
